Wednesday Code and Notes (Week 5)

1. Lecture Notes
2. Promela Examples

1 Lecture Notes

Synchronous channels:

  - send and receive must happen together

Asynchronous channels:

  A special case of asynch channels:
    reliable FIFO channels

  - send is non-blocking; puts a message in a queue
  - receive pops a message from a queue
    receive blocks if there aren't messages

Q: what happens if the queue is full:
A: varies from channel to channel
   It might:
   - block until there's space
       (that's what we implemented in Producer-Consumer)
   - drop messages if there's no space


Conway's problem example:

K = 5
Let's say the input is:

  aabaaaaabbaaaaaaaaaaaaaaaaabc .....

The output should be:
  2ab5a\n2b9a7\nabc ...


In a synchronous transition diagram,
 instead of having transitions

   l,l': starting location; destination location
   b: guard
   f: state update

   l -- b; f ---> l'

Now we'll have three kinds of transitions:

*internal transitions*

   l -- b; f ---> l'

*send transition*

   send x on ch; and also guard b; state update f

   l -- b; ch ⇐ x;f ---> l'

*receive transition*

   send x on ch; and also guard b; state update f

   l -- b; ch ⇒ x;f ---> l'

2 Promela Examples

2.1 Channel basics

Synchronous hello world:

/* a channel called ch
     with queue capacity 0 (synchronous)
     can transmit messages of type byte
 */ 
chan ch = [0] of { byte }

active proctype P() {
  ch ! 30; // send 30 on channel ch
  ch ! 55;
}

active proctype Q() {
  byte x=0;
  ch ? x; // receive a message on ch; save to xmi
  printf("I received: %d\n",x);
  ch ? x;
  printf("I received: %d\n",x);  
}

Asynchronous hello world:

/* a channel called ch
     with queue capacity 1 (asynchronous)
     can transmit messages of type byte
 */ 
chan ch = [1] of { byte }

active proctype P() {
  ch ! 30; // send 30 on channel ch
  ch ! 55;

  /* Two kinds of send:
       ch ! x  // put a message at the end of the queue
       ch !! x // "sort" a message into the queue     
     Four kinds of receive:
       ch ? x    // pop the first message from the queue
                    if it matches our pattern
       ch ? <x>  // read the first message from the queue
                    *without* removing it from the queue
       ch ?? x    // pop the first message from the queue
                     *that* matches our pattern
       ch ?? <x>  // read the first message from the queue
                     *that* matches our pattern
   */
}

active proctype Q() {
  byte x=0;
  ch ? x; // receive a message on ch; save to x
  printf("I received: %d\n",x);
  ch ? x;
  printf("I received: %d\n",x);  
}

Blocking vs non-blocking send:

chan ch = [0] of { byte }
chan ach = [5] of { byte }

active proctype P() {
  ch ! 30; // this send never happens; nobody is receiving and the channel is synchronous

  printf("** P sent a message!\n") // also never happens
}

active proctype R() {
  ach ! 30; // this send does happen; it goes in the queue

  printf("** R sent a message!\n")
}

2.2 Arithmetic server

/*
   b,x,y,ch

   b is true if you want to add; false if you want to subtract
   x y: the numbers you want to operate on
   ch: the channel you expect your reply on
 */
chan public = [0] of { bool, int, int, chan }

active proctype server() {
  int x;
  int y;
  chan session;
  do
       /* receive where we only accept messages where the bool component is 1 */
    :: public?1,x,y,session ->
       session!x+y
    :: public?0,x,y,session ->
       session!x-y
  od
  /* Q: will it block or go to the next branch?
     A: the do blocks until at least one branch is non-blocking
        when that happens, one of the non-blocking branches is chosen non-deterministically
   */
}

active proctype add_client() {
  chan add_channel = [0] of { int};
  int x = 0;
  public!1,1,1,add_channel;
  add_channel?x;
  printf("** 1 + 1 is %d, according to the server\n",x)
}

active proctype subtract_client() {
  chan subtract_channel = [0] of { int };
  int x = 0;
  public!0,1,1,subtract_channel;
  subtract_channel?x;
  printf("** 1 - 1 is %d, according to the server\n",x)
}

2.3 Conway's Problem

#define MAX 9
#define K 4

chan inC = [0] of { byte };
chan outC = [0] of { byte };
chan pipe = [0] of { byte };

proctype compress() {
  byte c = 0;
  byte previous = 0;
  byte n = 0;
  inC ? previous;
  do
  :: inC ? c;
     if
     :: c == previous && n < MAX - 1 ->
        n = n + 1;
     :: else ->
        if
        :: n > 0 ->
           pipe ! (n + 49);
           n = 0;
        :: else -> skip;
        fi;
        pipe ! previous;
        previous = c;
     fi;
  od;
}

proctype output() {
  byte c = 0;
  byte m = 0;
  do
  :: pipe ? c;
     outC ! c;
     m = m + 1;
     if
     :: m >= K ->
        outC ! 10;
        m = 0;
     :: else -> skip
     fi;
  od;
}

/* The sink just prints any characters it receives to stdout */
proctype sink() {
  byte c = 0;
  do
  :: outC ? c ->
     printf("%c",c);
  od;
}

/* Transmit the character sequence AAAAABC over and over */
proctype source() {
  do
  :: inC ! 65;
     inC ! 65;
     inC ! 65;
     inC ! 65;
     inC ! 65;     
     inC ! 66;
     inC ! 67;
  od;
}

init {
  run compress();
  run output();

  run source();
  run sink();
}

2.4 Multiplier (from Matrix transputer)

This is not a stand-alone model.

proctype Multiplier(byte Coeff;
                    chan North;
                    chan East;
                    chan South;
                    chan West)
{
  byte Sum, X;
  for (i : 0..(SIZE-1)) {
    if :: North ? X -> East ? Sum;
       :: East  ? Sum -> North ? X;
    fi;
    South ! X;
    Sum = Sum + X*Coeff;
    West  ! Sum;
  }
}

2.5 Dining philosophers

Note that this solution may deadlock, for the same reason as the lock-based solution we considered earlier.

You may check this by using Promela to search for invalid end-states.

You can apply the same fix as before to remedy this (imposing a total order on the forks to break the symmetry).

#define N 3

chan forks[N] = [0] of { bit };

inline think() {
  do
  :: true -> skip;
  :: true -> break;
  od
}

proctype philosopher(byte i) {
  do
  :: think();
     // pattern matching
     // receive the first message in the queue
     // but only if it equals true
     forks[i] ? true;
     forks[(i + 1) % N] ? true;
     // eat
     forks[i] ! true;
     forks[(i + 1) % N] ! true;
  od
}

proctype fork(byte i) {
  do
  :: forks[i] ! true;
     forks[i] ? true;
  od
}

init {
  byte i = 1;
  for(i : 1 .. N) {
    run philosopher(i-1);
    run fork(i-1);    
  }
}